$\forall$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type). Msg($M$) $\in$ Type